$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:$T$ List. insert($a$;$L$) $\in$ $T$ List